;;;============================================================================
;;;
;;; Subject: Standard Simplicial Set
;;;          
;;;
;;;----------------------------------------------------------------------------
;;;
;;; JHV 02-03-10
;;;
;;;============================================================================

(in-package "ACL2")

(set-verify-guards-eagerness 0)

(include-book "generic-kenzo-properties-imp2")

(include-book "increasing-list")

;;;==================================================
;;; EAT
;;;==================================================

(set-irrelevant-formals-ok t)

(defun face-delta-eat (n i gsm)
  (cond ((endp gsm) nil)
	((zp i) (cdr gsm))
	(t (cons (car gsm) (face-delta-eat n (- i 1) (cdr gsm))))
	))


(set-irrelevant-formals-ok nil)

#|

;;; Some Examples

(face-delta-eat 3 0 '(1 3 4 6)) = (3 4 6)
(face-delta-eat 3 1 '(1 3 4 6)) = (1 4 6)
(face-delta-eat 3 2 '(1 3 4 6)) = (1 3 6)
(face-delta-eat 3 3 '(1 3 4 6)) = (1 3 4)

|#


(defun canonical-delta-eat (absm)
  (increasing-p absm))


(defthm faceoface-delta-eat
  (implies (and (natp i)
		(natp j)
		(< i j)
		(canonical-delta-eat ls)
		)
	   (equal (face-delta-eat n i (face-delta-eat n j ls))
		  (face-delta-eat n (+ -1 j) (face-delta-eat n i ls))))
)



(defthm increasing-p-face-delta-eat-help
  (implies (and (increasing-p dgop)
		(natp d)
		(consp dgop))
	   (equal (car (face-delta-eat n d dgop))
		  (if (zp d)
		      (cadr dgop)
		    (car dgop))))
  )
  
(defthm increasing-p-face-delta-eat
  (implies (and (natp d)
		(increasing-p dgop))
	   (increasing-p (face-delta-eat n d dgop)))
  )
	   


#|
(definstance-*simplicial-set-kenzo*
  ((face face-delta-eat)
   (canonical canonical-delta-eat))
  "-delta-eat")
|#


;;;==================================================
;;; Binary
;;;==================================================

(set-irrelevant-formals-ok t)

(defun face-delta-binary-aux (n i gsm)
  (cond ((endp gsm) nil)
	((= i 0) 
	 (cond ((= (car gsm) 1) (cons 0 (cdr gsm)))
	       (t (cons (car gsm)
			(face-delta-binary-aux n i (cdr gsm)))))) 
	(t (cond ((= (car gsm) 1) 
		  (cons (car gsm)
			(face-delta-binary-aux n (1- i) (cdr gsm))))
	       (t (cons (car gsm)
			(face-delta-binary-aux n i (cdr gsm)))))
	   )
	))


(defun face-delta-binary (n i gsm)
  (face-delta-binary-aux n i gsm)) 


(defun final-face-delta-binary (n d dgop)
  (remove-final-zeros (face-delta-binary n d dgop)))

(set-irrelevant-formals-ok nil)

#|

(face-delta-binary-aux 3 0 '(0 1 0 1 1 0 1)) = (0 0 0 1 1 0 1)
(3 4 6)
(face-delta-binary-aux 3 1 '(0 1 0 1 1 0 1)) = (0 1 0 0 1 0 1)
(1 4 6)
(face-delta-binary-aux 3 2 '(0 1 0 1 1 0 1)) = (0 1 0 1 0 0 1)
(1 3 6)
(face-delta-binary-aux 3 3 '(0 1 0 1 1 0 1)) = (0 1 0 1 1 0 0)
(1 3 4)

|#

(encapsulate
 ()

(defun face-delta-binary-face-delta-eat-induct (n d dgop)
  (cond ((endp dgop) (list n d dgop))
	((= d 0) 
	 (cond ((= (car dgop) 1) (list n d dgop))
	       (t (face-delta-binary-face-delta-eat-induct n d (cdr dgop) )))) 
	(t (cond ((= (car dgop) 1) 
		  (face-delta-binary-face-delta-eat-induct n (1- d) (cdr dgop) ))
	       (t (face-delta-binary-face-delta-eat-induct n d (cdr dgop))))
	   )
	))


(local

 (defthm face-delta-binary=face-delta-eat-help1
  (implies (and (not (equal d 0))
		(natp d))
	   (equal (face-delta-eat n d '(0))
		  '(0))))


)



(local (defthm face-delta-binary=face-delta-eat-help2
  (implies (and (not (equal d 0))
		(natp d)
		(equal (car dgop) 1)
		(not (cdr dgop)))
	   (equal (face-delta-binary-aux n (- d) dgop)
		  '(1)))
 ))


(local (defthm face-delta-binary=face-delta-eat-help3
  (equal (1+ls (face-delta-eat n d dgop))
	 (face-delta-eat n d (1+ls dgop)))))

(local(defthm len=len-1+ls
  (equal (len (1+ls a)) (len a))))

(local(defthm append-1+ls-cdr
  (implies (consp dgop)
	   (equal (append (1+ls (cdr dgop)) '(0))
		  (cdr (append (1+ls dgop) '(0)))))))

(local(defthm consp-1+ls
  (implies (consp a)
	   (consp (1+ls a)))))

(local(defthm face-delta-binary=face-delta-eat-help4-1
 (implies (and (natp d)
	       (equal d 0)
	       (consp dgop)
	       (increasing-p dgop))
	  (equal (face-delta-eat n d (append (1+ls dgop) '(0)))
		 (append (1+ls (face-delta-eat n d dgop)) '(0))
		 )
	  )))

(local(defthm face-delta-binary=face-delta-eat-help4-2
 (implies (and (natp d)
	       (consp dgop)
	       (not (equal d (len dgop)))
	       (increasing-p dgop))
	  (equal (face-delta-eat n d (append (1+ls dgop) '(0)))
		 (append (1+ls (face-delta-eat n d dgop)) '(0))
		 )
	  )
 :hints (("Goal" :induct (face-delta-eat n d dgop)))))

 
(local(defthm face-delta-binary=face-delta-eat-help4-3
  (implies (not (equal (+ 1 d) (len (append (1+ls a) '(0)))))
	   (not (equal d (len a))))))



(local(defthm 1-+-1-d-len-append
  (equal (1- (+ -1 (- d) (len (append (1+ls a) '(0)))))
	 (+ -1 (- d) (len a)))))


(local (defthm face-delta-binary=face-delta-eat
 (implies (and (natp d) (dgb-p dgop))
	   (equal (dgb->increasing (face-delta-binary n d dgop))
		  (face-delta-eat n d (dgb->increasing dgop))))

 :hints (("Goal" :induct (FACE-DELTA-BINARY-FACE-DELTA-EAT-INDUCT N d DGOP))
	 )))


(local (defthm dgb-p=>quasi-dgb-p
	 (implies (dgb-p a)
		  (quasi-dgb-p a))
	 :rule-classes nil))

(local (defthm quasi-dgb-p-face-delta-binary
 (implies (and (natp d)
	       (dgb-p dgop))
	   (quasi-dgb-p (face-delta-binary n d dgop)))
 :hints (("Subgoal *1/2''" 
	  :use ((:instance dgb-p=>quasi-dgb-p (a (cdr dgop))))))
 ))


(local (defthm remove-final-zeros-face-delta-binary=face-delta-eat-help1
  (implies (and (natp d)
		(dgb-p dgop))
	   (equal (increasing->dgb (dgb->increasing (remove-final-zeros (face-delta-binary n d dgop))))
		  (increasing->dgb (face-delta-eat n d (dgb->increasing dgop)))))
  :hints (("Goal" :in-theory (disable increasing->dgb
				      dgb->increasing
				      face-delta-binary
				      face-delta-eat
				      remove-final-zeros)
	 :use ((:instance dgb->increasing-remove-final-zeros 
			  (dgop (face-delta-binary n d dgop)))))))
)


(local (defthm remove-final-zeros-face-delta-binary=face-delta-eat-help2
  (implies (and (natp d)
		(dgb-p dgop))
	   (equal (remove-final-zeros (face-delta-binary n d dgop))
		  (increasing->dgb (face-delta-eat n d (dgb->increasing dgop)))))
  :hints (("Goal" :in-theory (disable increasing->dgb
				      dgb->increasing
				      face-delta-binary
				      face-delta-eat
				      remove-final-zeros)
	 :use ((:instance quasi-dgb-to-dgb
		(dgb (face-delta-binary n d dgop)))
	       (:instance increasing->dgb-dgb->increasing (dgb (remove-final-zeros (face-delta-binary n d dgop))))
	       )))))



(defthm final-face-delta-binary=face-delta-eat
  (implies (and (natp d)
		(dgb-p dgop))
	   (equal (final-face-delta-binary n d dgop)
		  (increasing->dgb (face-delta-eat n d (dgb->increasing dgop))))
	   )
  :hints (("Goal" :in-theory (disable increasing->dgb
				      dgb->increasing
				      face-delta-binary
				      face-delta-eat
				      remove-final-zeros)
	 )))

)






(defun canonical-delta-binary (absm)
  (dgb-p absm))

(defthm faceoface-delta-binary
  (implies (and (natp i)
		(natp j)
		(< i j)
		(canonical-delta-binary ls))
	   (equal (final-face-delta-binary n i (final-face-delta-binary n j ls))
		  (final-face-delta-binary n (+ -1 j) (final-face-delta-binary n i ls))))
  :hints (("Goal" :in-theory (disable dgl->dgb
				      dgb->dgl
				      face-delta-binary
				      final-face-delta-binary
				      face-delta-eat
				      remove-final-zeros))))



#|

(in-theory (disable final-face-delta-binary))

(definstance-*simplicial-set-kenzo*
  ((face final-face-delta-binary)
   (canonical canonical-delta-binary))
  "-delta-binary")

|#


;;;===========================================================================
;;; Kenzo
;;;===========================================================================


#|

 Original Kenzo definition

(DEFUN DELTA-FACE (indx dmns gmsm)
   (declare
      (fixnum indx gmsm)
      (ignore dmns))
   (do ((pmark 1 (ash pmark 1))
           (bmark indx)
           (gmsm2 gmsm (ash gmsm2 -1)))
          (nil)
        (declare (fixnum pmark bmark gmsm2))
         (when (oddp gmsm2)
            (when (minusp (decf bmark))
               (return-from delta-face (logxor gmsm pmark)
			    )))))

;;; Some Examples

(delta-face 0 3 85) = 84
(delta-face 1 3 85) = 81
(delta-face 2 3 85) = 69
(delta-face 3 3 85) = 21

(delta-face 0 5 171) = 170
(delta-face 1 5 171) = 169
(delta-face 2 5 171) = 163
(delta-face 3 5 171) = 139
(delta-face 4 5 171) = 43
|#
 
(defun delta-face-do (pmark bmark gmsm2 gmsm)
  (declare (xargs :measure (if (and (natp bmark) (natp gmsm2)
				    (< bmark (logcount gmsm2)))
			       (+ bmark gmsm2)
			       0)
		  :hints (("Goal" :in-theory (enable ash)))))
  (if (and (natp bmark) (natp gmsm2)
	   (< bmark (logcount gmsm2)))
      (cond ((oddp gmsm2)
	     (cond ((minusp (1- bmark)) (logxor gmsm pmark))
		   (t (delta-face-do (ash pmark 1)
				     (1- bmark)
				     (ash gmsm2 -1)
				     gmsm))
		   ))
	     (t (delta-face-do (ash pmark 1)
			       bmark
			       (ash gmsm2 -1)
			       gmsm)))    
      gmsm
      ))


(defun delta-face (dmns indx gmsm)
  (declare (ignore dmns))
  (delta-face-do 1 indx gmsm gmsm))



#| Some examples

(delta-face 3 0 85) = 84
(delta-face 3 1 85) = 81
(delta-face 3 2 85) = 69
(delta-face 3 3 85) = 21

(delta-face 4 0 171) = 170
(delta-face 4 1 171) = 169
(delta-face 4 2 171) = 163
(delta-face 4 3 171) = 139
(delta-face 4 4 171) = 43

|#




(encapsulate 
 ()

(local (defthm car=1=>oddp
  (implies (and (equal (car dgop) 1)
		(dgb-p dgop))
	   (oddp (dgb->dgn dgop)))))

(local (defthm car=0=>evenp
  (implies (and (equal (car dgop) 0)
		(dgb-p dgop))
	   (evenp (dgb->dgn dgop)))))


(local(defthm logxor-1+ash-1
  (equal (logxor (+ 1 (ash a 1)) 1)
	 (ash a 1))
  :hints (("Goal"
	    :in-theory (enable evenp ash
			       logxor logeqv lognot logorc1 logior logand))))
      )


(local(defthm logcount-1+ash
  (implies (and (> a 0)
		(integerp a))
	   (> (logcount a) 0))	 
  :rule-classes :linear
  :hints (("Goal"
	    :in-theory (enable evenp ash logcount
			       logxor logeqv lognot logorc1 logior logand))))
      )

(local(defun face-delta-binary-aux=delta-face-do-induct (n d dgop pmark)
  (cond ((endp dgop) (list n d dgop pmark))
	((= d 0) 
	 (cond ((= (car dgop) 1) (list n d dgop pmark))
	       (t (face-delta-binary-aux=delta-face-do-induct n d (cdr dgop) (ash pmark 1) )))) 
	(t (cond ((= (car dgop) 1) 
		  (face-delta-binary-aux=delta-face-do-induct n (1- d) (cdr dgop) (ash pmark 1)))
	       (t (face-delta-binary-aux=delta-face-do-induct n d (cdr dgop) (ash pmark 1))))
	   )
	)))

(local(defthm natp-logcount=0=>0
  (implies (and (natp a)
		(equal (logcount (ash a 1)) 0))
	   (equal a 0))
  :rule-classes nil
  :hints (("Goal"
	    :in-theory (enable evenp ash logcount
			       logxor logeqv lognot logorc1 logior logand))))
      )

(local(defthm 0<a=>0<ash-a-1
  (implies (and (natp a) (< 0 a))
	   (< 0 (ash a 1)))))

(local(defthm 0<dgb->dgn
  (implies (and (dgb-p a)
		(not (endp a)))
	   (< 0 (dgb->dgn a)))
  :rule-classes :linear
  ))


(local(defthm 0=dgb->dgn
  (implies (and (dgb-p a)
		(endp a))
	   (equal 0 (dgb->dgn a)))
  :rule-classes :linear
  ))


(local(defthm 0=dgb->dgn=>endp
  (implies (and (dgb-p a)
		(equal 0 (dgb->dgn a)))
	   (endp a))
  ))



(local(defthm face-delta-eat-len<=d
  (implies (and (natp d)
		(increasing-p dgop)
		(<= (len dgop) d))
	   (equal (face-delta-eat n d dgop)
		  dgop))))

(local(defthm len=len-1+ls
  (equal (len (1+ls a))
	 (len a))))

(local(defthm len+1=len-append
  (equal (+ 1 (len a))
	 (len (append (1+ls a) '(0))))))


(local(defthm dgb-p-len-count
  (implies (dgb-p dgop)
	   (<= 0 (len-count dgop)))))


(local(defthm dgb-p-car-len-count
  (implies (and (dgb-p dgop)
		(equal (car dgop) 1)
		(not (endp dgop)))
	   (equal (len-count dgop)
		  (1+ (len-count (cdr dgop)))))))


(local(defthm dgb-p-car-len-count-1
  (implies (and (dgb-p dgop)
		(equal (car dgop) 1)
		(not (endp dgop)))
	   (< 0 (len-count dgop)))))
  
(local(defthm 0<len-append
  (< 0 (len (append (1+ls a) '(0))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance len+1=len-append))))))


(local(defthm face-delta-binary-len-count<=d
  (implies (and (natp d)
		(dgb-p dgop)
		(<= (len-count dgop) d))
	   (equal (face-delta-binary-aux n d dgop)
		  dgop))
  :hints (("Subgoal *1/2.2" :do-not-induct t
	   :use ((:instance 0<len-append
			    (a (dgb->dgl (cdr dgop)))))))))


(local(defthm logcount=len-count
  (implies (dgb-p dgop)
	   (equal (logcount (dgb->dgn dgop))
		  (len-count dgop)))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance logcount=len-count-1
			    (dgop (dgb->dgn dgop))
				   ))))))

(local(defthm face-delta-binary-logcount<=d
  (implies (and (natp d)
		(dgb-p dgop)
		(<= (logcount (dgb->dgn dgop)) d))
	   (equal (face-delta-binary-aux n d dgop)
		  dgop))
  ))

(local(defthm len-count-cdr<=len-count
  (implies (dgb-p dgop)
	   (<= (len-count (cdr dgop))
	       (len-count dgop)))
 ))

(local(defthm len-count-cdr<=len-count-car
  (implies (and (dgb-p dgop)
		(equal (car dgop) 1))
	   (< (len-count (cdr dgop))
	       (len-count dgop)))
 ))


(local(defthm logcount-cdr<=logcount
  (implies (dgb-p dgop)
	   (<= (logcount (dgb->dgn (cdr dgop)))
	       (logcount (dgb->dgn dgop))))
 :hints (("Goal" :use
	  ((:instance logcount=len-count (dgop (cdr dgop)))
	   (:instance logcount=len-count (dgop dgop))
	   (:instance len-count-cdr<=len-count))))))

(local(defthm logcount-cdr<=logcount-car
  (implies (and (dgb-p dgop)
		(equal (car dgop) 1))
	   (< (logcount (dgb->dgn (cdr dgop)))
	       (logcount (dgb->dgn dgop))))
 :hints (("Goal" :use
	  ((:instance logcount=len-count (dgop (cdr dgop)))
	   (:instance logcount=len-count (dgop dgop))
	   (:instance len-count-cdr<=len-count-car))))))


(local(defthm face-delta-binary-logcount<=d-cdr
  (implies (and (natp d)
		(dgb-p dgop)
		(<= (logcount (dgb->dgn dgop)) d))
	   (equal (face-delta-binary-aux n d (cdr dgop))
		  (cdr dgop)))
  :hints (("Goal" :use
	  ((:instance logcount-cdr<=logcount)
	   (:instance face-delta-binary-logcount<=d (dgop (cdr dgop)))
	   )))))

(local(defthm face-delta-binary-logcount<=d-cdr-car
  (implies (and (natp d)
		(dgb-p dgop)
		(equal (car dgop) 1)
		(<= (logcount (dgb->dgn dgop)) d))
	   (equal (face-delta-binary-aux n (1- d) (cdr dgop))
		  (cdr dgop)))
  :hints (("Goal" :use
	  ((:instance logcount-cdr<=logcount-car)
	   (:instance face-delta-binary-logcount<=d (dgop (cdr dgop)))
	   )))))


(local(defthm face-delta-binary-aux=delta-face-do-help1
  (implies (and (natp d)
		(natp dgop)
		(natp dgop2)
		(natp pmark))
	   (equal (delta-face-do (ash pmark 1) d dgop2 (ash dgop 1))
		  (ash (delta-face-do pmark d dgop2 dgop) 1))))
      )
      
(local(defthm face-delta-binary-aux=delta-face-do-help2-aux
  (implies (and (natp d)
		(natp dgop)
		(natp dgop2)
		(natp pmark))
	   (equal (delta-face-do (ash pmark 1) d dgop2 (1+ (ash dgop 1)))
		  (1+ (ash (delta-face-do pmark d dgop2 dgop) 1))))
  :hints (("Goal" :in-theory (disable LOGXOR-1-EVENP-EVENP ash-logxor+1))))
      )

(local(defthm face-delta-binary-aux=delta-face-do-help2
  (implies (and (natp d)
		(not (equal d 0))
		(natp dgop)
		(natp dgop2)
		(natp pmark))
	   (equal (delta-face-do (ash pmark 1) (1- d) dgop2 (1+ (ash dgop 1)))
		  (1+ (ash (delta-face-do pmark (1- d) dgop2 dgop) 1))))
 ))

(local(defthm face-delta-binary-aux=delta-face-do-sol1-help1
  (implies (and (dgb-p dgop)
		(natp d)
		(not (equal d 0))
		(equal (dgb->dgn (face-delta-binary-aux n d dgop))
		       (delta-face-do 1 d (dgb->dgn dgop) (dgb->dgn dgop))))
	   (equal (ash (dgb->dgn (face-delta-binary-aux n d dgop)) 1)
		  (ash (delta-face-do 1 d (dgb->dgn dgop) (dgb->dgn dgop)) 1))))
      )
      
(local(defthm face-delta-binary-aux=delta-face-do-sol1-help2
  (implies (and (dgb-p dgop)
		(natp d)
		(not (equal d 0)))
	   (equal (ash (delta-face-do 1 d (dgb->dgn dgop) (dgb->dgn dgop)) 1)
		  (delta-face-do 2 d (dgb->dgn dgop) (ash (dgb->dgn dgop) 1))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable FACE-DELTA-BINARY-AUX=DELTA-FACE-DO-SOL1-HELP1)
	   :use ((:instance natp-dgb->dgn (dgb dgop))
		 (:instance face-delta-binary-aux=delta-face-do-sol1-help1)
		 (:instance face-delta-binary-aux=delta-face-do-help1
			    (pmark 1) (dgop2 (dgb->dgn dgop))
			    (dgop (dgb->dgn dgop))))))))


(local(defthm face-delta-binary-aux=delta-face-do-sol1
  (implies (and (dgb-p dgop)
		(natp d)
		(not (equal d 0))
		(equal (dgb->dgn (face-delta-binary-aux n d dgop))
		       (delta-face-do 1 d (dgb->dgn dgop) (dgb->dgn dgop))))
	   (equal (delta-face-do 2 d (dgb->dgn dgop) (ash (dgb->dgn dgop) 1))
		  (ash (dgb->dgn (face-delta-binary-aux n d dgop)) 1)))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable FACE-DELTA-BINARY-AUX=DELTA-FACE-DO-SOL1-HELP1
			       FACE-DELTA-BINARY-AUX=DELTA-FACE-DO-SOL1-HELP2)
	   :use ((:instance face-delta-binary-aux=delta-face-do-sol1-help1)
		 (:instance face-delta-binary-aux=delta-face-do-sol1-help2))
	   ))))



(local(defthm face-delta-binary-aux=delta-face-do-sol2-help1
  (implies (and (dgb-p dgop)
		(natp d)
		(not (equal d 0))
		(equal (dgb->dgn (face-delta-binary-aux n (1- d) dgop))
		       (delta-face-do 1 (1- d) (dgb->dgn dgop) (dgb->dgn dgop))))
	   (equal (1+ (ash (dgb->dgn (face-delta-binary-aux n (1- d) dgop)) 1))
		  (1+ (ash (delta-face-do 1 (1- d) (dgb->dgn dgop) (dgb->dgn dgop)) 1)))))
)

(local(defthm face-delta-binary-aux=delta-face-do-sol2-help2
  (implies (and (dgb-p dgop)
		(natp d)
		(not (equal d 0)))
	   (equal (1+ (ash (delta-face-do 1 (1- d) (dgb->dgn dgop) (dgb->dgn dgop)) 1))
		  (delta-face-do 2 (1- d) (dgb->dgn dgop) (1+ (ash (dgb->dgn dgop) 1)))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable FACE-DELTA-BINARY-AUX=DELTA-FACE-DO-SOL2-HELP1)
	   :use ((:instance natp-dgb->dgn (dgb dgop))
		 (:instance face-delta-binary-aux=delta-face-do-sol2-help1)
		 (:instance face-delta-binary-aux=delta-face-do-help2
			    (pmark 1) (dgop2 (dgb->dgn dgop))
			    (dgop (dgb->dgn dgop))))))))


(local(defthm face-delta-binary-aux=delta-face-do-sol2
  (implies (and (dgb-p dgop)
		(natp d)
		(not (equal d 0))
		(equal (dgb->dgn (face-delta-binary-aux n (1- d) dgop))
		       (delta-face-do 1 (1- d) (dgb->dgn dgop) (dgb->dgn dgop))))
	   (equal (delta-face-do 2 (1- d) (dgb->dgn dgop) (1+ (ash (dgb->dgn dgop) 1)))
		  (1+ (ash (dgb->dgn (face-delta-binary-aux n (1- d) dgop)) 1))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable FACE-DELTA-BINARY-AUX=DELTA-FACE-DO-SOL2-HELP1
		    FACE-DELTA-BINARY-AUX=DELTA-FACE-DO-SOL2-HELP2
		    )
	   :use ((:instance face-delta-binary-aux=delta-face-do-sol2-help1)
		 (:instance face-delta-binary-aux=delta-face-do-sol2-help2))
	   ))))


(local(defthm face-delta-binary-aux=delta-face-do-sol3-help1
  (implies (and (dgb-p dgop)
		(natp d)
		(equal (dgb->dgn (face-delta-binary-aux n d dgop))
		       (delta-face-do 1 d (dgb->dgn dgop) (dgb->dgn dgop))))
	   (equal (ash (dgb->dgn (face-delta-binary-aux n d dgop)) 1)
		  (ash (delta-face-do 1 d (dgb->dgn dgop) (dgb->dgn dgop)) 1))))
      )

(local(defthm face-delta-binary-aux=delta-face-do-sol3-help2
  (implies (and (dgb-p dgop)
		(natp d))
	   (equal (ash (delta-face-do 1 d (dgb->dgn dgop) (dgb->dgn dgop)) 1)
		  (delta-face-do 2 d (dgb->dgn dgop) (ash (dgb->dgn dgop) 1))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable FACE-DELTA-BINARY-AUX=DELTA-FACE-DO-SOL3-HELP1)
	   :use ((:instance natp-dgb->dgn (dgb dgop))
		 (:instance face-delta-binary-aux=delta-face-do-sol3-help1)
		 (:instance face-delta-binary-aux=delta-face-do-help1
			    (pmark 1) (dgop2 (dgb->dgn dgop))
			    (dgop (dgb->dgn dgop))))))))

(local(defthm face-delta-binary-aux=delta-face-do-sol3
  (implies (and (dgb-p dgop)
		(natp d)		
		(equal (dgb->dgn (face-delta-binary-aux n d dgop))
		       (delta-face-do 1 d (dgb->dgn dgop) (dgb->dgn dgop))))
	   (equal (delta-face-do 2 d (dgb->dgn dgop) (ash (dgb->dgn dgop) 1))
		  (ash (dgb->dgn (face-delta-binary-aux n d dgop)) 1)))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable FACE-DELTA-BINARY-AUX=DELTA-FACE-DO-SOL3-HELP1
			       FACE-DELTA-BINARY-AUX=DELTA-FACE-DO-SOL3-HELP2)
	   :use ((:instance face-delta-binary-aux=delta-face-do-sol3-help1)
		 (:instance face-delta-binary-aux=delta-face-do-sol3-help2))
	   ))))

(local(defthm face-delta-binary-aux=delta-face-do
  (implies (and (natp d)
		(dgb-p dgop))
	   (equal (dgb->dgn (face-delta-binary-aux n d dgop))
		  (delta-face-do 1 d (dgb->dgn dgop) (dgb->dgn dgop))))
  
:hints (("Goal"
	 :in-theory (disable FACE-DELTA-BINARY-AUX=DELTA-FACE-DO-SOL3-HELP1
			     FACE-DELTA-BINARY-AUX=DELTA-FACE-DO-SOL3-HELP2
			     FACE-DELTA-BINARY-AUX=DELTA-FACE-DO-SOL1-HELP1
			       FACE-DELTA-BINARY-AUX=DELTA-FACE-DO-SOL1-HELP2
			       FACE-DELTA-BINARY-AUX=DELTA-FACE-DO-SOL2-HELP1
			       FACE-DELTA-BINARY-AUX=DELTA-FACE-DO-SOL2-HELP2) ))

))

(local(defthm face-delta-binary=delta-face-1
  (implies (and (natp d)
		(dgb-p dgop))
	   (equal (dgb->dgn (face-delta-binary n d dgop))
		  (delta-face n d (dgb->dgn dgop))))
  ))

(local(defthm dgb-p=>quasi-dgb-p
	 (implies (dgb-p a)
		  (quasi-dgb-p a))
	 :rule-classes nil))


(local(defthm quasi-dgb-p-face-delta-binary
 (implies (and (natp d)
	       (dgb-p dgop))
	   (quasi-dgb-p (face-delta-binary n d dgop)))
 :hints (("Subgoal *1/2''" 
	  :use ((:instance dgb-p=>quasi-dgb-p (a (cdr dgop))))))
 ))

(local(defthm final-face-delta-binary=delta-face-1
  (implies (and (natp d)
		(dgb-p dgop))
	   (equal (dgb->dgn (remove-final-zeros (face-delta-binary n d dgop)))
		  (delta-face n d (dgb->dgn dgop))
	   ))
  :hints (("Goal" :in-theory (disable dgn->dgb
				      dgb->dgn
				      face-delta-binary
				      delta-face
				      remove-final-zeros)
	 :use ((:instance dgb->dgn-remove-final-zeros 
			  (dgop (face-delta-binary n d dgop))))))
  ))


(local(defthm final-face-delta-binary=delta-face-2
  (implies (and (natp d)
		(natp dgop))
	   (equal (dgb->dgn (remove-final-zeros (face-delta-binary n d (dgn->dgb dgop))))
		  (delta-face n d dgop)))
  :hints (("Goal" :in-theory (disable dgn->dgb
				      dgb->dgn
				      face-delta-binary
				      delta-face
				      remove-final-zeros)
	  ))
  ))


(defthm final-face-delta-binary=delta-face
  (implies (and (natp d)
		(natp dgop))
	   (equal (delta-face n d dgop)
		  (dgb->dgn (final-face-delta-binary n d (dgn->dgb dgop)))
	    ))
  :hints (("Goal" :in-theory (disable dgn->dgb
				      dgb->dgn
				      face-delta-binary
				      delta-face
				      remove-final-zeros)
	  ))
  )

)


(defun canonical-delta-kenzo (dgop)
  (natp dgop))

(defthm faceoface-delta
  (implies (and (natp i)
		(natp j)
		(< i j)
		(canonical-delta-kenzo ls))
	   (equal (delta-face n i (delta-face n j ls))
		  (delta-face n (+ -1 j) (delta-face n i ls))))
  :hints (("Goal" :in-theory (disable dgn->dgb
				      dgb->dgn
				      delta-face
				      face-delta-binary
				      final-face-delta-binary
				      face-delta-eat
				      remove-final-zeros))))



#|

(in-theory (disable delta-face))

(definstance-*simplicial-set-kenzo*
  ((face delta-face)
   (canonical canonical-delta-kenzo))
  "-delta")

;;;----------------------------------------------------------------------------
;;;
;;; The properties:
;;;
;;;----------------------------------------------------------------------------


(pe 'kenzo-property-1-delta)

(pe 'kenzo-property2-delta)

(pe 'kenzo-property-3-delta)

(pe 'kenzo-property-4-delta)

(pe 'kenzo-property-4-a-delta)

(pe 'kenzo-property-5-delta)


|#



